Spécification et analyse d'un protocole de contrôle d'accès optimiste pour éditeurs collaboratifs répartis
Identifieur interne : 000E28 ( Main/Exploration ); précédent : 000E27; suivant : 000E29Spécification et analyse d'un protocole de contrôle d'accès optimiste pour éditeurs collaboratifs répartis
Auteurs : Aurel Randolph [Canada] ; Abdessamad Imine [France] ; Hanifa Boucheneb [Canada] ; Alejandro Quintero [Canada]Source :
- Ingénierie des systèmes d'information : (2001) [ 1633-1311 ] ; 2014.
Descripteurs français
- Pascal (Inist)
- Protocole accès, Sécurité informatique, Protocole transmission, Système conversationnel, Réplication, Synchronisation, Mise à jour, Accès document, Spécification formelle, Synthèse commande, Conception ingénierie, Conception intégrée, Commande répartie, Temps accès, Autorisation, Politique, Exécution programme, Retard, Facteur humain, Ingénierie simultanée, ., Contrôle accès, Edition collaborative, Vérification formelle.
- Wicri :
- topic : Politique.
English descriptors
- KwdEn :
- Access control, Access protocol, Access time, Collaborative edition, Computer security, Concurrent engineering, Control synthesis, Delay, Distributed control, Document access, Engineering design, Formal specification, Formal verification, Human factor, Integrated design, Interactive system, Licence procedure, Policy, Program execution, Replication, Synchronization, Transmission protocol, Updating.
Abstract
Distributed Collaborative Editors are interactive systems where several and dispersed users edit concurrently shared documents. Generally, these systems rely on data replication and use safe synchronization protocol which ensures data consistency even though the users's updates are executed in any order on different copies. Controlling access in such systems is a challenging problem, as they need dynamic access changes and low latency access to shared documents. In (Imine et al., 2009), a flexible access control protocol is proposed; it is based on replicating the shared document and its authorization policy at the local memory of each user. To deal with latency and dynamic access changes, an optimistic access control technique is used where enforcement of authorizations is retroactive. However, verifying whether the combination of access control and synchronization protocol preserves the data consistency is a hard task since it requires examining a large number of situations. In this paper, we show how to specify and verify formally an access control protocol designed for Distributed Collaborative Editor. The analysis let to conclude that the protocol preserves consistency in such a way that the access control policy is enforced identically at all participating user sites. Most importantly, this analysis enables us to validate some conceptual choices of the protocol.
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream PascalFrancis, to step Corpus: 000002
- to stream PascalFrancis, to step Curation: 000A01
- to stream PascalFrancis, to step Checkpoint: 000003
- to stream Main, to step Merge: 000E20
- to stream Main, to step Curation: 000E28
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="fr" level="a">Spécification et analyse d'un protocole de contrôle d'accès optimiste pour éditeurs collaboratifs répartis</title><author><name sortKey="Randolph, Aurel" sort="Randolph, Aurel" uniqKey="Randolph A" first="Aurel" last="Randolph">Aurel Randolph</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>École Polytechnique de Montréal</s1><s2>Montréal</s2><s3>CAN</s3><sZ>1 aut.</sZ><sZ>3 aut.</sZ><sZ>4 aut.</sZ></inist:fA14><country>Canada</country><placeName><settlement type="city">Montréal</settlement><region type="state">Québec</region></placeName></affiliation></author><author><name sortKey="Imine, Abdessamad" sort="Imine, Abdessamad" uniqKey="Imine A" first="Abdessamad" last="Imine">Abdessamad Imine</name><affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Université de Lorraine et INRIA-LORIA</s1><s2>Nancy-Grand-Est</s2><s3>FRA</s3><sZ>2 aut.</sZ></inist:fA14><country>France</country><wicri:noRegion>Nancy-Grand-Est</wicri:noRegion><wicri:noRegion>Université de Lorraine et INRIA-LORIA</wicri:noRegion><wicri:noRegion>Université de Lorraine et INRIA-LORIA</wicri:noRegion></affiliation></author><author><name sortKey="Boucheneb, Hanifa" sort="Boucheneb, Hanifa" uniqKey="Boucheneb H" first="Hanifa" last="Boucheneb">Hanifa Boucheneb</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>École Polytechnique de Montréal</s1><s2>Montréal</s2><s3>CAN</s3><sZ>1 aut.</sZ><sZ>3 aut.</sZ><sZ>4 aut.</sZ></inist:fA14><country>Canada</country><placeName><settlement type="city">Montréal</settlement><region type="state">Québec</region></placeName></affiliation></author><author><name sortKey="Quintero, Alejandro" sort="Quintero, Alejandro" uniqKey="Quintero A" first="Alejandro" last="Quintero">Alejandro Quintero</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>École Polytechnique de Montréal</s1><s2>Montréal</s2><s3>CAN</s3><sZ>1 aut.</sZ><sZ>3 aut.</sZ><sZ>4 aut.</sZ></inist:fA14><country>Canada</country><placeName><settlement type="city">Montréal</settlement><region type="state">Québec</region></placeName></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">INIST</idno><idno type="inist">15-0038007</idno><date when="2014">2014</date><idno type="stanalyst">PASCAL 15-0038007 INIST</idno><idno type="RBID">Pascal:15-0038007</idno><idno type="wicri:Area/PascalFrancis/Corpus">000002</idno><idno type="wicri:Area/PascalFrancis/Curation">000A01</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000003</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000003</idno><idno type="wicri:doubleKey">1633-1311:2014:Randolph A:specification:et:analyse</idno><idno type="wicri:Area/Main/Merge">000E20</idno><idno type="wicri:Area/Main/Curation">000E28</idno><idno type="wicri:Area/Main/Exploration">000E28</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="fr" level="a">Spécification et analyse d'un protocole de contrôle d'accès optimiste pour éditeurs collaboratifs répartis</title><author><name sortKey="Randolph, Aurel" sort="Randolph, Aurel" uniqKey="Randolph A" first="Aurel" last="Randolph">Aurel Randolph</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>École Polytechnique de Montréal</s1><s2>Montréal</s2><s3>CAN</s3><sZ>1 aut.</sZ><sZ>3 aut.</sZ><sZ>4 aut.</sZ></inist:fA14><country>Canada</country><placeName><settlement type="city">Montréal</settlement><region type="state">Québec</region></placeName></affiliation></author><author><name sortKey="Imine, Abdessamad" sort="Imine, Abdessamad" uniqKey="Imine A" first="Abdessamad" last="Imine">Abdessamad Imine</name><affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Université de Lorraine et INRIA-LORIA</s1><s2>Nancy-Grand-Est</s2><s3>FRA</s3><sZ>2 aut.</sZ></inist:fA14><country>France</country><wicri:noRegion>Nancy-Grand-Est</wicri:noRegion><wicri:noRegion>Université de Lorraine et INRIA-LORIA</wicri:noRegion><wicri:noRegion>Université de Lorraine et INRIA-LORIA</wicri:noRegion></affiliation></author><author><name sortKey="Boucheneb, Hanifa" sort="Boucheneb, Hanifa" uniqKey="Boucheneb H" first="Hanifa" last="Boucheneb">Hanifa Boucheneb</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>École Polytechnique de Montréal</s1><s2>Montréal</s2><s3>CAN</s3><sZ>1 aut.</sZ><sZ>3 aut.</sZ><sZ>4 aut.</sZ></inist:fA14><country>Canada</country><placeName><settlement type="city">Montréal</settlement><region type="state">Québec</region></placeName></affiliation></author><author><name sortKey="Quintero, Alejandro" sort="Quintero, Alejandro" uniqKey="Quintero A" first="Alejandro" last="Quintero">Alejandro Quintero</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>École Polytechnique de Montréal</s1><s2>Montréal</s2><s3>CAN</s3><sZ>1 aut.</sZ><sZ>3 aut.</sZ><sZ>4 aut.</sZ></inist:fA14><country>Canada</country><placeName><settlement type="city">Montréal</settlement><region type="state">Québec</region></placeName></affiliation></author></analytic><series><title level="j" type="main">Ingénierie des systèmes d'information : (2001)</title><title level="j" type="abbreviated">Ing. syst. inf. : (2001)</title><idno type="ISSN">1633-1311</idno><imprint><date when="2014">2014</date></imprint></series></biblStruct></sourceDesc><seriesStmt><title level="j" type="main">Ingénierie des systèmes d'information : (2001)</title><title level="j" type="abbreviated">Ing. syst. inf. : (2001)</title><idno type="ISSN">1633-1311</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Access control</term><term>Access protocol</term><term>Access time</term><term>Collaborative edition</term><term>Computer security</term><term>Concurrent engineering</term><term>Control synthesis</term><term>Delay</term><term>Distributed control</term><term>Document access</term><term>Engineering design</term><term>Formal specification</term><term>Formal verification</term><term>Human factor</term><term>Integrated design</term><term>Interactive system</term><term>Licence procedure</term><term>Policy</term><term>Program execution</term><term>Replication</term><term>Synchronization</term><term>Transmission protocol</term><term>Updating</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Protocole accès</term><term>Sécurité informatique</term><term>Protocole transmission</term><term>Système conversationnel</term><term>Réplication</term><term>Synchronisation</term><term>Mise à jour</term><term>Accès document</term><term>Spécification formelle</term><term>Synthèse commande</term><term>Conception ingénierie</term><term>Conception intégrée</term><term>Commande répartie</term><term>Temps accès</term><term>Autorisation</term><term>Politique</term><term>Exécution programme</term><term>Retard</term><term>Facteur humain</term><term>Ingénierie simultanée</term><term>.</term><term>Contrôle accès</term><term>Edition collaborative</term><term>Vérification formelle</term></keywords><keywords scheme="Wicri" type="topic" xml:lang="fr"><term>Politique</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Distributed Collaborative Editors are interactive systems where several and dispersed users edit concurrently shared documents. Generally, these systems rely on data replication and use safe synchronization protocol which ensures data consistency even though the users's updates are executed in any order on different copies. Controlling access in such systems is a challenging problem, as they need dynamic access changes and low latency access to shared documents. In (Imine et al., 2009), a flexible access control protocol is proposed; it is based on replicating the shared document and its authorization policy at the local memory of each user. To deal with latency and dynamic access changes, an optimistic access control technique is used where enforcement of authorizations is retroactive. However, verifying whether the combination of access control and synchronization protocol preserves the data consistency is a hard task since it requires examining a large number of situations. In this paper, we show how to specify and verify formally an access control protocol designed for Distributed Collaborative Editor. The analysis let to conclude that the protocol preserves consistency in such a way that the access control policy is enforced identically at all participating user sites. Most importantly, this analysis enables us to validate some conceptual choices of the protocol.</div></front></TEI><affiliations><list><country><li>Canada</li><li>France</li></country><region><li>Québec</li></region><settlement><li>Montréal</li></settlement></list><tree><country name="Canada"><region name="Québec"><name sortKey="Randolph, Aurel" sort="Randolph, Aurel" uniqKey="Randolph A" first="Aurel" last="Randolph">Aurel Randolph</name></region><name sortKey="Boucheneb, Hanifa" sort="Boucheneb, Hanifa" uniqKey="Boucheneb H" first="Hanifa" last="Boucheneb">Hanifa Boucheneb</name><name sortKey="Quintero, Alejandro" sort="Quintero, Alejandro" uniqKey="Quintero A" first="Alejandro" last="Quintero">Alejandro Quintero</name></country><country name="France"><noRegion><name sortKey="Imine, Abdessamad" sort="Imine, Abdessamad" uniqKey="Imine A" first="Abdessamad" last="Imine">Abdessamad Imine</name></noRegion></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000E28 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 000E28 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= Pascal:15-0038007
|texte= Spécification et analyse d'un protocole de contrôle d'accès optimiste pour éditeurs collaboratifs répartis
}}
| This area was generated with Dilib version V0.6.33. |  |